R:Realizer, y, i:Id. read-restricted(R; i; y)  R-has-loc(R;i) 

latex

Definitions	t  T, P  Q, x:A. B(x), b, Realizer, Id, read-restricted(R; i; y)
Lemmas	assert wf, read-restricted wf, Id wf, es realizer wf, R-occurs-has-loc, read-restricted-R-occurs